es:ES, ff:FIFO, f2f+:F2F+-decls, sndr, rcvr:ff.C, e, e':E.
f2f+-pred(e',e)  [e: rcvr is_ack  sndr]  [e': sndr is_req   rcvr] 

latex

Definitions	left + right, x:A. B(x), t  T, {T}, x:A  B(x), b, ES, FIFO, F2F+-decls, let a,b,c,d,e,f,g = u in v(a;b;c;d;e;f;g), ff.C, t.1, E, s = t, A, [e: i p j], e c e', f2f+-pred(e',e), f(a), A c B, P & Q, P  Q, is_ack , [e: i p j], is_req  , P  Q, False
Lemmas	f2f+-property, ack-pred-req, f2f+Ack wf, f2f+-pred wf, es-E wf, fifoC wf, F2F+-decls wf, FIFO wf, event system wf, f2f+-pred-closed, snd-it wf, f2f+Req wf